Kaman协议的形式化验证

doi:10. 3969/j. issn. 1006-2475.2012.04.005

计算机与现代化 ›› 2012, Vol. 1 ›› Issue (200): 17-06.doi: 10. 3969/j. issn. 1006-2475.2012.04.005

Kaman协议的形式化验证

文双举

甘肃省高等学校招生办公室，甘肃兰州 730030

收稿日期:2012-02-06 修回日期:1900-01-01 出版日期:2012-04-16 发布日期:2012-04-16

Formal Verification of Kaman Protocol

WEN Shuang-ju

High-level School Admissions Office of Gansu Province， Lanzhou 730030， China

Received:2012-02-06 Revised:1900-01-01 Online:2012-04-16 Published:2012-04-16

摘要/Abstract

摘要： Kaman协议是移动Ad Hoc网络安全认证机制，然而，协议设计者未对该协议的安全性作严格的形式化分析。协议复合逻辑PCL是验证协议安全属性的形式化方法，PCL逻辑能够简化协议安全分析过程。本文在协议复合逻辑PCL中描述Kaman协议并分析Kaman协议的安全属性，证明Kaman协议能够实现其安全目标。

关键词: 移动Ad Hoc网络, 协议复合逻辑, Kaman协议

Abstract:

Kaman is security authentication scheme of mobile Ad Hoc networks. However， the author of Kaman didn’t verify security of the protocol by using formal method. Protocol Composition Logic （PCL） is formal verification logic of security protocol. This logic can simplify the process of protocol verification. This paper describes Kaman and analyzes its security properties in PCL. It is proved that Kaman can implement its security aim.

Key words: Ad Hoc networks, protocol composition logic, Kaman protocol

文双举. Kaman协议的形式化验证[J]. 计算机与现代化, 2012, 1(200): 17-06.

WEN Shuang-ju. Formal Verification of Kaman Protocol[J]. Computer and Modernization, 2012, 1(200): 17-06.

Kaman协议的形式化验证

Formal Verification of Kaman Protocol

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 1

编辑推荐

Metrics

本文评价